\begin{tabbing}
rv{-}disjoint($p$;$n$;$X$;$Y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:\{0..$n$$^{-}$\}.\+
\\[0ex]($\forall$$s_{1}$:(\{0..$n$$^{-}$\}$\rightarrow$p{-}outcome($p$)), $s_{2}$:(\{0..$n$$^{-}$\}$\rightarrow$p{-}outcome($p$)).
\\[0ex]($\forall$$j$:\{0..$n$$^{-}$\}. ($\neg$($j$ = $i$ $\in$ $\mathbb{Z}$)) $\Rightarrow$ ($s_{1}$($j$) = $s_{2}$($j$) $\in$ p{-}outcome($p$)))
\\[0ex]$\Rightarrow$ ($X$($s_{1}$) = $X$($s_{2}$) $\in$ $\mathbb{Q}$))
\\[0ex]$\vee$ \=($\forall$$s_{1}$:(\{0..$n$$^{-}$\}$\rightarrow$p{-}outcome($p$)), $s_{2}$:(\{0..$n$$^{-}$\}$\rightarrow$p{-}outcome($p$)).\+
\\[0ex]($\forall$$j$:\{0..$n$$^{-}$\}. ($\neg$($j$ = $i$ $\in$ $\mathbb{Z}$)) $\Rightarrow$ ($s_{1}$($j$) = $s_{2}$($j$) $\in$ p{-}outcome($p$)))
\\[0ex]$\Rightarrow$ ($Y$($s_{1}$) = $Y$($s_{2}$) $\in$ $\mathbb{Q}$))
\-\-
\end{tabbing}